Formal property checking has gained significant importance in System-on-Chip (SoC) verification and has become part of many industrial design flows. Unfortunately, arithmetic circuits with multiplication have always been and to some extent remain the show-stopper for formal property checking in industrial practice. Satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE.
Neither satisfiability (SAT) solving nor decision diagrams of any sort provide robust and universal frameworks to deal with arithmetic. Specialized “engineering” solutions are available that adapt to specific scenarios in equivalence checking or property checking. Most of these methods depend on exploiting specific high-level arithmetic information. This can be useful for highly regular designs as they may result from automatic module generation. However, for full-custom logic design, the problem has remained unsolved.
When designing arithmetic units for high-performance applications, a designer will usually start implementing a basic version of the algorithm. At this point, word-level abstractions are still available in the design. However, as aggressive timing requirements have to be met, the initial algorithm has to be modified and optimized by a series of manual steps involving transformations at all levels. Such a full-custom implementation is not only of high complexity, its specialized structure makes it difficult to apply any kind of abstraction above the Boolean bit-level.
Obviously, designs resulting from such a manual optimization process may contain errors which are hard to find and which will surface late in the design cycle and may not be found by simulation or emulation. Even after many years, and in spite of substantial progress in formal verification, functional correctness of full-custom arithmetic has remained a major concern in SoC design flows.
Multipliers have become very common in today's designs of processors, digital signal processors, hardware accelerators and other signal processing devices. While standard property checking usually fails for such designs, in industrial practice it is often attempted to verify these designs by equivalence checking against some reference. This can work well if reference and design have a large amount of structural similarities and share many functionally equivalent signals. But, if design and reference have different architectures, the equivalence check immediately becomes impossible.
In the context of verifying floating-point-units (FPUs) their embedded multipliers are separated from formal approaches, e.g. by so called black boxing and checking by simulation as described in the paper of C. Jacobi et al., “Automatic Verification of Fused Multiply-Add FPUs” published in Design, Automation and Test in Europe 2005, Proceedings, vol. 2, pp. 1298-1303.
Multipliers lack a compact canonical representation that can be built efficiently from gate level implementations. A BDD (BDD=a Binary Decision Diagram) is a data structure for representing Boolean functions. For ROBDDs (ROBDD=Reduced Ordered BDD), it is well-known that the number of nodes grows exponentially with the number of input bits to the multiplier. Even if binary decision diagrams (BDDs) are not directly used to build the multiplier outputs but only certain internal relations, they lack robustness and suffer from BDD node explosion. For instance, A. Kuehlmann et al., “Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification”, published in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, December 2005, vol. 21, pp. 1377-1394, discloses a combination of techniques for Boolean reasoning based on BDDs, structural transformations an SAT procedure and random simulation natively working on a shared graph representation of the problems of formal equivalence checking and property verification as well as other CAD applications (CAD=Computer Aided Design).
There have been several attempts to solve the multiplier verification problem with different variants of decision diagrams. Word level decision diagrams called BMDs (BMD=Binary Moment Diagram) can be used to efficiently represent integer multiplication. A *BMD (star-BMD) is a multiplicative BMD with the particular characteristic to grow linearly for multiplication. In a *BMD, the number of nodes to represent integer multiplication only grows linearly in contrast to the exponential growth of a BDD. Several improvements have been made, but the main obstacle remains—BMDs require word level information about the design which usually is not available or is very hard to extract from highly optimized gate level descriptions being typical in high performance applications. When building *BMDs for such highly irregular multipliers, the same node explosion can be observed during the construction process as for BDDs, in spite of the theoretical result that the final representation will be compact.
In the paper of D. Stoffel and W. Kunz “Verification of integer multipliers on the arithmetic bit level”, published in ICCAD 2001, pp. 183-189, an equivalent network of bit adders is extracted from a gate level description of arithmetic circuits. Equivalence between two extracted networks is proven by a simple calculus. In the paper of M. Wedler et al., “Normalization at the arithmetic bit level”, published in Proceedings of the 42nd Design Automation Conference, June 2005, pp. 457-462, this work is extended towards applications in property checking. A normalization process is provided that creates structural similarities between the design under verification and the specification given as a property. However, it is assumed that not only the property but also the design is specified at the arithmetic bit level or higher levels of abstraction. Both approaches rely on the successful extraction of the arithmetic bit level information. This is possible for synthesized netlists, but in full-custom design the situation is different. Manual architectural changes and full-custom optimizations may involve global transformations. Extraction of an arithmetic bit-level description can turn out to be quite difficult since there are an exponential number of possible decompositions.